Step of Proof: not_functionality_wrt_iff
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
not
functionality
wrt
iff
:
P
,
Q
:
. (
P
Q
)
((
P
)
(
Q
))
latex
by ((((((Unfold `not` 0)
CollapseTHEN (GenUnivCD))
)
CollapseTHENM (HypBackchain))
)
Co
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C
) inil_term)))
latex
C
.
Definitions
t
T
,
P
Q
,
P
Q
,
A
,
P
Q
,
P
Q
,
,
x
:
A
.
B
(
x
)
Lemmas
iff
wf
,
false
wf
origin